$\forall$$i$,$x$:Id, $T$:Type, $L$:(Knd List).
\\[0ex]normal{-}type\{i:l\}($T$) $\Rightarrow$ R{-}realizes\{i:l\}(Rframe($i$; $T$; $x$; $L$); ${\it es}$.frame{-}p(${\it es}$; $i$; $T$; $x$; $L$))